% \section{Background}
% \label{section:background}

%\subsection{Model Transformations}
% \subsection{Transforming Models With Graph Rewriting}
% \label{subsec:model_transformations}
% 
% \mf{ {\bf Michalis and Levi do} Description of what it means to do model
% transformation (very high level)}
% 
% \mf{TODO: the following need to be reworded to avoid text replication with
% ICSE14}
% 
% In this paper we consider models to be attributed, typed graphs.  A {\em
% transformation} is a program that takes one model as an input and produces
% another model as its output. There are many kinds of model
% transformations~\cite{czarnecki03} but in this paper we focus on
% transformations based on graph rewriting~\cite{ehrig06}.
% The basic building block of such transformations is the {\em transformation
% rule}, defined as follows:
% 
% \BD[Transformation rule]
% A {\em transformation rule} $R$ is a tuple $R=\tuple{\set{$\rp{NAC}$}$,\rp{LHS},\rp{RHS}$}$,
% where  \rp{LHS} and \rp{RHS} are the typed graphs called
%  the {\em left-hand} and
% the {\em right-hand} sides of the rule, respectively, and $\set{\rp{NAC}}$ represents a (potentially
% empty) set of typed graphs called the {\em negative application conditions}.
% \ED
% 
% \mf{TODO: we need an example rule, preferrably from the VCS2Autosar example.}
% Fig.~\ref{?} depicts the \rp{NAC}s, \rp{LHS} and \rp{RHS}
% of the rule $R_{F}$ from Fig.~\ref{?}
% as typed graphs using types from the UML metamodel~\cite{UML10}.
% \mf{TODO: update}
% For example, \rp{NAC}1 consists of a state \name{x} with an entry action
% \name{a1} that is a UML \name{behaviour} (e.g., a class operation).
% 
% The \rp{NAC}s, \rp{LHS}, and \rp{RHS} of a rule consist of different {\em parts}, i.e., sets of
% model elements which do not necessarily form proper graphs.  These parts play different
% roles during the rule application:
% \begin{description}
% \item [\rC:] The set of model elements that are present both in the \rp{LHS} and the
% \rp{RHS}, i.e.,
% remain unaffected by the rule.
% \item [\rD:] The set of elements in the \rp{LHS} that are absent in the \rp{RHS}, i.e.,
% deleted by the rule.
% \item [\rA:] The set of elements present in the \rp{RHS} but absent in the \rp{LHS}, i.e.,
% added by the rule.
% \item [\rN:] The set of elements present in any \rp{NAC},  but not those
% present in \rC.
% \end{description}
% 
% 
% In our example, the parts are as follows: ... 
% \mf{TODO, when we agree on example rule}.
% % For the example rule $R_{F}$ from Fig.~\ref{fig:foldentry}, these parts are as follows: \rC~is
% % $\set{$\name{x},\name{x1},\name{x2},\name{a},\name{t1},\name{t1\_x1},\name{t1\_x},
% % \name{t2},\name{t2\_x2},\name{t2\_x}$}$,\\ \rD~is the set
% % $\set{$\name{t1\_a},\name{t2\_a}$}$, \rA~is the set $\set{$\name{x\_a}$}$,
% % \rN~is set
% % $\set{$\name{a1},\name{x\_a1},\name{x3},\name{t3},\name{t3\_x3},\name{t3\_x}$}$.
% % To reduce clutter, only \rD and \rA are explicitly indicated in the figure.
% 
% A rule $R$ is {\em applied} to a model $M$ by finding a {\em matching site}
% of its \rp{LHS} in $M$:
%  
% \BD[Matching site] \label{def:matchsite}
% A \emph{matching site} of a transformation rule $R$ in a model $M$ is a tuple
% $K=\tuple{$\mN,\mC,\mD$}$, where \mC~and \mD~are matches of the parts \rC~and
% \rD~of the \rp{LHS} of $R$ in $M$, and \mN~is the set of all matches of
% \rp{NAC}s in $M$ relative to \mC~and \mD .
% \ED
% 
% \mf{TODO: once we settle on example, we should illustrate this on the example.
% Can reuse commented out latex code.}
% 
% % \begin{table}[t!]
% % \caption{Matching sites of rule $R_F$ in Fig.~\ref{fig:foldentry} for the domain model in Fig.~\ref{fig:wash}.}
% % \label{fig:msites}
% % {\small 
% % \begin{center}
% % \begin{tabular}{|p{0.5cm}|p{1.2cm}|p{3.1cm}|p{2.0cm}|}
% % \hline {\bf Site} & {\bf \mN} & {\bf \mC} & {\bf \mD}  \\
% % \hline 
% % $K_1$ & \name{Washing}, \name{TempCheck}
% % & \parbox{3.1cm}{
% % \begin{flushleft}
% % \vspace{-0cm}
% % \name{Washing}, \name{Locking}, \name{Waiting},
% % \name{wash.Start()}, \name{lw}, \name{lw\_Locking},
% %  \name{lw\_Washing}, \name{ww}, \name{ww\_Waiting}, \name{ww\_Washing}
% % \end{flushleft}
% % }
% % &  \name{lw\_wash.Start()}, \name{ww\_wash.Start()}
% %  \\
% % \hline $K_2$ &
% % &
% % \parbox{3.1cm}{
% % \begin{flushleft}
% % \name{UnLocking}, \name{Washing}, \name{Drying},
% % \name{QuickCool()}, \name{wu}, \name{wu\_Washing},
% %  \name{wu\_UnLocking}, \name{du}, \name{du\_Drying}, \name{du\_UnLocking}
% % \end{flushleft}
% % }
% % &
% % \name{wu\_QuickCool()}, \name{du\_QuickCool()} 
% % \\
% % \hline
% % \end{tabular}
% % \end{center}}
% % \vspace{-0.2in}
% % \end{table}
% % Two matching sites for the rule $R_{F}$ in the washing machine
% % controller in Fig.~\ref{fig:wash} are shown in Table~\ref{fig:msites} 
% % (two more matches, isomorphic to $K_1$ and $K_2$, are not shown for brevity).
% % In this table,
% % \name{lw} and \name{ww} are the names of the transitions between states
% % \name{Locking}/\name{Waiting} and \name{Washing}; while \name{wu} and \name{du}
% % are the names of the transitions between states \name{Washing}/ \name{Drying} and
% % \name{UnLocking}.  The table says, for example, that in part \mD~of matching
% % site $K_1$, \name{t1\_a}=\name{lw\_wash.Start()} and \name{t2\_a}=
% % \name{ww\_wash.Start()}.
% 
% 
% 
% In the above definition, \mN~denotes the set of all matches within model $M$ of the
% \rp{NAC}s of $R$ given the match of \rC~and \rD. If the same \rp{NAC} can match multiple
% ways, then all of them are included in \mN~as separate matches.  
% \mf{TODO: update:}
% For example, if state \name{Washing} had another input transition, that
% transition would also appear in \mN~for $K_1$ since it would match $t3$.
% 
% The set of matching sites define those places in the model where the rule can
% potentially be applied:
% \BD[Applicability condition]\label{def:rulecond}
% Given a transformation rule $R$, a model $M$, and a matching site
% $K = \tuple{$\mN, \mC, \mD$}$,  $R$ is \emph{applicable at $K$}
% iff \mN~is empty\footnote{The theory of graph
% transformation requires some additional formal preconditions, most notably, the
% {\em gluing condition}~\cite{ehrig06}. We so not discuss them here
% for brevity.}.
% \ED
% The above definition ensures that the rule can only be applied at a given site
% if \mC~and \mD~are matched and no \rp{NAC} is matched.
% \mf{Update:}	
% For $R_{F}$, the matching
% site $K_1$ given in Table~\ref{fig:msites} does not satisfy the
% applicability condition since \mN$_1 \not = \emptyset$.  On the other hand,
% no \rp{NAC}s hold in the second matching site, $K_2$.
% 
% \begin{figure}[t]
% \begin{minipage}[t]{3in}
% \begin{tabbing}
% b \= bll \= bl \= bl \= bl \= bl \= bl \= bl \= bl \= (Distinctttt) \= \kill
% \\
% \textbf{Algorithm: Apply Rule} \\
% \textbf{Input}: Rule $R$, model $M$, matching site $K= \tuple{$\mN, \mC, \mD$}$\\
% \textbf{Output}: Transformed model $M'$\\
% \> 1: \> $M' = M$ \\
% \> 2: \> {\bf if} \mN~$=\emptyset$ {\bf then} \\
% \> 3: \> \> {\bf let} \mA~ be a set of fresh elements corresponding\\
% \> \> \> \>  to the part \rA~of $R$ \\
% \> 4: \> \> add \mA~to $M'$, \\
% \> 5: \> \> remove \mD~from $M'$ \\
% \> 6: \> {\bf return} $M'$
% \end{tabbing}
% \vspace{-0.15in}
% \end{minipage}
% \caption{Algorithm for applying a graph transformation rule.}
% \label{alg:classical}
% \vspace{-0.1in}
% \end{figure}
% 
% \mf{Added term:}
% We call rule appliation at a specific matching site that satisfies the
% applicability condition, a {\em production}. 
% 
% The rule application algorithm is given in Fig.~\ref{alg:classical}.
% The applicability condition is checked in Step 2 and if it satisfied, the rule
% is applied by adding the elements in \mA~(Step 4) and deleting the elements in
% \mD~(Step 5). 
% \mf{TODO: update with example}
% For example, applying $R_{F}$ to $K_2$ requires the deletion of the action
% \name{QuickCool()} from the two transitions because it is contained in \mD, and
% the addition of \name{QuickCool()} as an entry action for state
% \name{UnLocking} according to \rA.
% 
% We refer to rules such as the ones described above as \emph{classical}, to
% differentiate them from their \emph{lifted} counterparts which can be applied to
% product lines.





